Definitions | False, {x:A| B(x)} , left + right, P Q, Dec(P), Void, let x,y = A in B(x;y), t.1, E, t T, b, AbsInterface(A), f(a), P  Q, x:A. B(x), X(e), s = t, , x:A B(x), x:A B(x), P & Q, x:A. B(x), Type, e c e', <a, b>, Unit, can-apply(f;x), e  X, Q ==f== P, E(X), Inj(A;B;f), f is Q-R-pre-preserving on P, {I}, Q  = f== P, g glues Ia:Qa  f Ib:Rb, Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), p-first(L), ES, Top, [], , x.A(x) |